MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { #equal(@x, @y) -> #eq(@x, @y)
  , *(@x, @y) -> #mult(@x, @y)
  , -(@x, @y) -> #sub(@x, @y)
  , div(@x, @y) -> #div(@x, @y)
  , eratos(@l) -> eratos#1(@l)
  , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs)))
  , eratos#1(nil()) -> nil()
  , filter(@p, @l) -> filter#1(@l, @p)
  , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x)
  , filter#1(nil(), @p) -> nil()
  , filter#2(@xs', @p, @x) ->
    filter#3(#equal(mod(@x, @p), #0()), @x, @xs')
  , mod(@x, @y) -> -(@x, *(@y, div(@x, @y)))
  , filter#3(#false(), @x, @xs') -> ::(@x, @xs')
  , filter#3(#true(), @x, @xs') -> @xs' }
Weak Trs:
  { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #eq(::(@x_1, @x_2), nil()) -> #false()
  , #eq(nil(), ::(@y_1, @y_2)) -> #false()
  , #eq(nil(), nil()) -> #true()
  , #eq(#0(), #0()) -> #true()
  , #eq(#0(), #s(@y)) -> #false()
  , #eq(#0(), #neg(@y)) -> #false()
  , #eq(#0(), #pos(@y)) -> #false()
  , #eq(#s(@x), #0()) -> #false()
  , #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
  , #eq(#neg(@x), #0()) -> #false()
  , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
  , #eq(#neg(@x), #pos(@y)) -> #false()
  , #eq(#pos(@x), #0()) -> #false()
  , #eq(#pos(@x), #neg(@y)) -> #false()
  , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
  , #mult(#0(), #0()) -> #0()
  , #mult(#0(), #neg(@y)) -> #0()
  , #mult(#0(), #pos(@y)) -> #0()
  , #mult(#neg(@x), #0()) -> #0()
  , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
  , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #0()) -> #0()
  , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
  , #sub(@x, #0()) -> @x
  , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y))
  , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y))
  , #div(#0(), #0()) -> #divByZero()
  , #div(#0(), #neg(@y)) -> #0()
  , #div(#0(), #pos(@y)) -> #0()
  , #div(#neg(@x), #0()) -> #divByZero()
  , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y))
  , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y))
  , #div(#pos(@x), #0()) -> #divByZero()
  , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y))
  , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y))
  , #add(#0(), @y) -> @y
  , #add(#neg(#s(#0())), @y) -> #pred(@y)
  , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
  , #add(#pos(#s(#0())), @y) -> #succ(@y)
  , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #and(#false(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#true(), #false()) -> #false()
  , #and(#true(), #true()) -> #true()
  , #natdiv(#0(), #0()) -> #divByZero()
  , #natdiv(#0(), #s(@y)) -> #0()
  , #natdiv(#s(@x), #0()) -> #divByZero()
  , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y))
  , #positive(#0()) -> #0()
  , #positive(#s(@x)) -> #pos(#s(@x))
  , #positive(#neg(@x)) -> #neg(@x)
  , #positive(#pos(@x)) -> #pos(@x)
  , #negative(#0()) -> #0()
  , #negative(#s(@x)) -> #neg(#s(@x))
  , #negative(#neg(@x)) -> #pos(@x)
  , #negative(#pos(@x)) -> #neg(@x)
  , #divsub(#0(), #0()) -> #0()
  , #divsub(#0(), #s(@y)) -> #underflow()
  , #divsub(#s(@x), #0()) -> #s(@x)
  , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y)
  , #natmult(#0(), @y) -> #0()
  , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y))
  , #natadd(#0(), @y) -> @y
  , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y))
  , #natdiv'(#0(), @y) -> #s(#0())
  , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y))
  , #natdiv'(#underflow(), @y) -> #0()
  , #natsub(@x, #0()) -> @x
  , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'linear polynomial interpretation' failed due to the following
      reason:
      
      The input cannot be shown compatible
   


Arrrr..